// Incrementally parse result from clasp (simple vesion)
// to compile: g++ -I/opt/local/include parser.cpp

#include <iostream>
#include <string>
#include <sstream>
#include <fstream>

#include <boost/optional.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix_core.hpp>
#include <boost/spirit/include/phoenix_operator.hpp>
#include <boost/spirit/include/phoenix_object.hpp>
#include <boost/spirit/include/phoenix_fusion.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>
#include <boost/spirit/include/phoenix_stl.hpp>
#include <boost/algorithm/string/trim.hpp>
#include <boost/shared_ptr.hpp>

namespace qi = boost::spirit::qi;
namespace ascii = boost::spirit::ascii;
namespace phoenix = boost::phoenix;

typedef std::vector<int> IntVec;
typedef boost::shared_ptr<IntVec> IntVecPtr;
typedef std::string::const_iterator forward_iterator_type;

// The Grammar
template <typename Iterator>
struct ClaspResultGrammar : qi::grammar<Iterator, ascii::space_type>
{

  ClaspResultGrammar(IntVecPtr& V_)
    : ClaspResultGrammar::base_type(model), V(V_)
  {
    using qi::int_;
    using qi::char_;
    using qi::_1;
    using phoenix::push_back;
    using phoenix::ref;

    sentinel = char_('0');
    
    literal = int_ - sentinel;

    model = +literal[push_back(ref(*V), _1)] >> sentinel;
  }

  qi::rule<Iterator, ascii::space_type> model;
  qi::rule<Iterator, ascii::space_type> sentinel;
  qi::rule<Iterator, int(), ascii::space_type> literal;

  IntVecPtr& V;
};


int 
main()
{
  std::ifstream claspfile("result.sat");

  if (claspfile.is_open())
    {
 
      std::string line;

      while (!claspfile.eof())
	{
	  bool complete = false;
	  IntVecPtr v(new IntVec);
	  ClaspResultGrammar<forward_iterator_type> crg(v);
	  
	  while (!complete)
	    {
	      getline(claspfile, line);
	      std::cout << "Processing: " << line << std::endl;

	      
	      forward_iterator_type beg = line.begin();
	      forward_iterator_type end = line.end();
	      
	      complete = qi::phrase_parse(beg, end, crg, ascii::space);
	      if (complete)
		{
		  std::cout << "Parse succeeded!" << std::endl;
		  std::copy(v->begin(), v->end(), std::ostream_iterator<int>(std::cout, " "));
		  std::cout << std::endl;
		}
	      else
		{
		  std::cout << "Parse failed!" << std::endl;
		}
	    }
	}
    }
  else
    {
      std::cout << "Unable to open result.sat" << std::endl;
    }
}
